(declare-sort S0 0)

(declare-fun _substvar_29_ () Real)
(declare-fun _substvar_31_ () Real)
(declare-const r0 Real)
(push)
(assert (<= r0 _substvar_31_ 1.0 r0))
(check-sat)
(assert (exists ((q14 Real) (q15 S0) (q16 S0) (q17 Real)) (distinct q17 0.1919438545 0.0)))
(push)
(pop)
(pop)
(assert (<= r0 _substvar_29_ 1.0 r0))
(check-sat)
